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  3611  preddowncl  6290  ssimaex  6919  onfununi  8274  oaordex  8486  domtriord  9054  findcard3  9186  unfilem1  9208  fodomfibOLD  9234  inf0  9533  inf3lem3  9542  tcel  9655  fidomtri2  9909  alephval3  10023  zorn2lem6  10414  fodomb  10439  eqreznegel  12875  iserodd  16797  cshwsiun  17061  txcn  23601  ssfg  23847  fclsnei  23994  eldmgm  26999  fnrelpredd  35250  cvmlift2lem10  35510  axtco1from2  36673  bj-axreprepsep  37398  relcnveq3  38662  iss2  38679  elrelscnveq3  38962  jca3  39316  prjspreln0  43056  omabs2  43778  tfsconcatrn  43788  rfovcnvf1od  44449  mnuop3d  44716  ssclaxsep  45427