Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  jca2 Structured version   Visualization version   GIF version

Theorem jca2 518
 Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)
Hypotheses
Ref Expression
jca2.1 (𝜑 → (𝜓𝜒))
jca2.2 (𝜓𝜃)
Assertion
Ref Expression
jca2 (𝜑 → (𝜓 → (𝜒𝜃)))

Proof of Theorem jca2
StepHypRef Expression
1 jca2.1 . 2 (𝜑 → (𝜓𝜒))
2 jca2.2 . . 3 (𝜓𝜃)
32a1i 11 . 2 (𝜑 → (𝜓𝜃))
41, 3jcad 517 1 (𝜑 → (𝜓 → (𝜒𝜃)))
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ∧ wa 400 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8 This theorem depends on definitions:  df-bi 210  df-an 401 This theorem is referenced by:  rr19.28v  3582  preddowncl  6154  ssimaex  6738  onfununi  7989  oaordex  8195  domtriord  8685  findcard3  8787  unfilem1  8808  fodomfib  8824  inf0  9110  inf3lem3  9119  tcel  9213  fidomtri2  9449  alephval3  9563  zorn2lem6  9954  fodomb  9979  eqreznegel  12367  iserodd  16220  cshwsiun  16484  txcn  22319  ssfg  22565  fclsnei  22712  eldmgm  25699  fnrelpredd  32583  cvmlift2lem10  32783  relcnveq3  36011  iss2  36034  elrelscnveq3  36164  jca3  36425  prjspreln0  39938  rfovcnvf1od  41071  mnuop3d  41345
 Copyright terms: Public domain W3C validator