Users' Mathboxes Mathbox for Jarvin Udandy < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  H15NH16TH15IH16 Unicode version

Theorem H15NH16TH15IH16 28045
Description: Given 15 hypotheses and a 16th hypothesis, there exists a proof the 15 imply the 16th. (Contributed by Jarvin Udandy, 8-Sep-2016.)
Hypotheses
Ref Expression
H15NH16TH15IH16.1  |-  ph
H15NH16TH15IH16.2  |-  ps
H15NH16TH15IH16.3  |-  ch
H15NH16TH15IH16.4  |-  th
H15NH16TH15IH16.5  |-  ta
H15NH16TH15IH16.6  |-  et
H15NH16TH15IH16.7  |-  ze
H15NH16TH15IH16.8  |-  si
H15NH16TH15IH16.9  |-  rh
H15NH16TH15IH16.10  |-  mu
H15NH16TH15IH16.11  |-  la
H15NH16TH15IH16.12  |-  ka
H15NH16TH15IH16.13  |- jph
H15NH16TH15IH16.14  |- jps
H15NH16TH15IH16.15  |- jch
H15NH16TH15IH16.16  |- jth
Assertion
Ref Expression
H15NH16TH15IH16  |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  /\  si )  /\  rh )  /\  mu )  /\  la )  /\  ka )  /\ jph )  /\ jps )  /\ jch
)  -> jth )

Proof of Theorem H15NH16TH15IH16
StepHypRef Expression
1 H15NH16TH15IH16.16 . 2  |- jth
21a1i 10 1  |-  ( ( ( ( ( ( ( ( ( ( ( ( ( ( ( ph  /\  ps )  /\  ch )  /\  th )  /\  ta )  /\  et )  /\  ze )  /\  si )  /\  rh )  /\  mu )  /\  la )  /\  ka )  /\ jph )  /\ jps )  /\ jch
)  -> jth )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 358
This theorem was proved from axioms:  ax-1 5  ax-mp 8
  Copyright terms: Public domain W3C validator