Theorem jctild 525

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctild.1	⊢ (𝜑 → (𝜓 → 𝜒))
jctild.2	⊢ (𝜑 → 𝜃)

Assertion

Ref	Expression
jctild	⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 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:  anc2li  555  equvini  2453  2reu1  3860  frpoinsg  6316  ordunidif  6382  isofrlem  7315  dfwe2  7750  orduniorsuc  7805  tfisg  7830  poxp  8107  fnse  8112  ssenen  9115  dffi3  9382  fpwwe2lem12  10595  zmulcl  12582  rpneg  12985  rexuz3  15315  cau3lem  15321  climrlim2  15513  o1rlimmul  15585  iseralt  15651  gcdzeq  16522  isprm3  16653  vdwnnlem2  16967  ablfaclem3  20019  epttop  22896  lmcnp  23191  dfconn2  23306  txcnp  23507  cmphaushmeo  23687  isfild  23745  cnpflf2  23887  flimfnfcls  23915  alexsubALT  23938  fgcfil  25171  bcthlem5  25228  ivthlem2  25353  ivthlem3  25354  dvfsumrlim  25938  plypf1  26117  noetalem1  27653  noseqinds  28187  axeuclidlem  28889  usgr2wlkneq  29686  wwlksnredwwlkn0  29826  wwlksnextwrd  29827  clwlkclwwlklem2a1  29921  lnon0  30727  hstles  32160  mdsl1i  32250  atcveq0  32277  atcvat4i  32326  cdjreui  32361  issgon  34113  connpconn  35222  outsideofrflx  36115  isbasisrelowllem1  37343  isbasisrelowllem2  37344  poimirlem3  37617  poimirlem29  37643  poimir  37647  heicant  37649  equivtotbnd  37772  ismtybndlem  37800  cvrat4  39437  linepsubN  39746  pmapsub  39762  osumcllem4N  39953  pexmidlem1N  39964  dochexmidlem1  41454  cantnfresb  43313  harval3  43527  clcnvlem  43612  relpfrlem  44943  iccpartimp  47418  sbgoldbwt  47778  sbgoldbst  47779  elsetrecslem  49688