Theorem jca2 523

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  rr19.28v  3625  preddowncl  6361  ssimaex  7001  onfununi  8387  oaordex  8604  domtriord  9180  findcard3  9312  unfilem1  9335  inf0  9659  inf3lem3  9668  tcel  9781  fidomtri2  10114  alephval3  10228  zorn2lem6  10618  fodomb  10644  eqreznegel  13101  iserodd  17057  cshwsiun  17321  txcn  24000  ssfg  24246  fclsnei  24393  eldmgm  27406  ordunmax  35833  fnrelpredd  35845  cvmlift2lem10  36285  axtco1from2  37478  bj-axreprepsep  38261  pibt2  38608  relcnveq3  39525  iss2  39542  elrelscnveq3  39825  jca3  40179  prjspreln0  43903  omabs2  44595  tfsconcatrn  44605  rfovcnvf1od  45265  mnuop3d  45516  ssclaxsep  46236