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  3619  preddowncl  6287  ssimaex  6916  onfununi  8270  oaordex  8482  domtriord  9047  findcard3  9178  unfilem1  9200  fodomfibOLD  9226  inf0  9522  inf3lem3  9531  tcel  9644  fidomtri2  9898  alephval3  10012  zorn2lem6  10403  fodomb  10428  eqreznegel  12838  iserodd  16754  cshwsiun  17018  txcn  23561  ssfg  23807  fclsnei  23954  eldmgm  26979  fnrelpredd  35174  cvmlift2lem10  35428  relcnveq3  38432  iss2  38449  elrelscnveq3  38712  jca3  39028  prjspreln0  42767  omabs2  43489  tfsconcatrn  43499  rfovcnvf1od  44161  mnuop3d  44428  ssclaxsep  45139