Theorem jca2 513

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 512	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  rr19.28v  3618  preddowncl  6274  ssimaex  6902  onfununi  8256  oaordex  8468  domtriord  9031  findcard3  9162  unfilem1  9184  fodomfibOLD  9210  inf0  9506  inf3lem3  9515  tcel  9628  fidomtri2  9882  alephval3  9996  zorn2lem6  10387  fodomb  10412  eqreznegel  12827  iserodd  16742  cshwsiun  17006  txcn  23536  ssfg  23782  fclsnei  23929  eldmgm  26954  fnrelpredd  35094  cvmlift2lem10  35348  relcnveq3  38355  iss2  38372  elrelscnveq3  38528  jca3  38895  prjspreln0  42642  omabs2  43365  tfsconcatrn  43375  rfovcnvf1od  44037  mnuop3d  44304  ssclaxsep  45015