Theorem jca2 514

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

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 513	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 396

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 206  df-an 397

This theorem is referenced by:  rr19.28v  3623  preddowncl  6291  ssimaex  6931  onfununi  8292  oaordex  8510  domtriord  9074  findcard3  9236  findcard3OLD  9237  unfilem1  9261  fodomfib  9277  inf0  9566  inf3lem3  9575  tcel  9690  fidomtri2  9939  alephval3  10055  zorn2lem6  10446  fodomb  10471  eqreznegel  12868  iserodd  16718  cshwsiun  16983  txcn  23014  ssfg  23260  fclsnei  23407  eldmgm  26408  fnrelpredd  33782  cvmlift2lem10  33993  relcnveq3  36855  iss2  36878  elrelscnveq3  37026  jca3  37391  prjspreln0  41005  omabs2  41725  tfsconcatrn  41735  rfovcnvf1od  42398  mnuop3d  42673