Theorem expr 367

Description: Export a wff from a right conjunct. (Contributed by Jeff Hankins, 30-Aug-2009.)

Hypothesis

Ref	Expression
expr.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

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

Proof of Theorem expr

Step	Hyp	Ref	Expression
1		expr.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	exp32 357	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	imp 122	1 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106

This theorem is referenced by:  reximddv  2465  rexlimdvaa  2479  issod  4082  ordsuc  4314  fcof1  5454  riota5f  5523  ovmpt2df  5663  tfrlemi1  5981  eqsuptid  6469  eqinftid  6493  ordiso2  6505  addnq0mo  6699  mulnq0mo  6700  genprndl  6773  genprndu  6774  addlocpr  6788  ltexprlemm  6852  ltexprlemopl  6853  ltexprlemopu  6855  ltexprlemfl  6861  ltexprlemfu  6863  aptiprleml  6891  caucvgprprlemexbt  6958  addsrmo  6982  mulsrmo  6983  prodge0  7999  un0addcl  8388  un0mulcl  8389  iseqfveq2  9544  iseqshft2  9548  monoord  9551  iseqsplit  9554  iseqid2  9564  expnegzap  9607  expcanlem  9740  ibcval5  9787  caucvgrelemcau  10004  cau3lem  10138  dvds0lem  10350  dvdsnegb  10357  dvdssub2  10382  isprm6  10670